COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00007 00003	.require "memo.pub[let,jmc]" source
C00010 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.bb EXTENSIONAL FORMS

	Consider first ordinary forms, i.e. expressions built
from symbols for constants, variables and functions and possibly
quantifiers and the Church lambda operator.  Such a form will
have certain free variables, and its value will depend on the
values assigned to the free variables.  We call two forms
⊗extensionally ⊗equivalent if they have the same value for all
assignments of values to the free variables they contain.  Thus
if + has its usual interpretation on the integers, the
forms ⊗x+y and ⊗y+x are extensionally equivalent, but neither of
them is extensionally equivalent to ⊗u+v, because assigning ⊗x 
and ⊗y the value 0 and ⊗u and ⊗v the value 1 gives the forms
different values.

	Extensional forms can be regarded as the equivalence classes of this
equivalence relation, but instead of first introducing ordinary forms
and the equivalence relation, we will define extensional forms inductively
from the symbols for constants, variables, and functions.  In order to
motivate the reader's attention to a somewhat boring inductive
definition, we remark on the following virtues of extensional forms:
First they have no bound variables which simplifies the statement of
the laws of substitution, and second all the ways of building up
extensional forms are by the application of functions to constituent
forms; even ⊗λ(x,e) is just a function of two extensional forms ⊗x 
and ⊗e.  Consequently the syntax and semantics of extensional forms
can be axiomatized in first order logic.  This is important for the
applications to mathematical theory of computation and to the theory
of concepts.

	We start with a simplified theory:

	Let ⊗D be a domain, e.g. the integers or people or concepts
of integers or concepts of people.  Let ⊗V be an infinite class of
objects called variables, and let ⊗E be another class of objects
called environments.  Let %2value: V %8x%2 E → D%1 be a distinguished
function.  We will call %2value(x,e)%1 the value of the variable ⊗x
in the environment ⊗e. We assume an axiom of extensionality for
environments, namely

Ext!!ext1:	%2∀e1 e2.(∀x.(value(x,e1) = value(x,e2)) ⊃ e1 = e2)%1.

Ext{eq ext1} implies that environments can be identified with certain
functions from variables to domain elements.  However, we cannot conclude
that all such functions are represented by environments.

	Next we have the assignment function %2assign: V %8x%2 D %8x%2 E → E%1.
It satisfies the axioms

Ext!!ext2:	%2∀x d e.(value(x,assign(x,d,e)) = d)%1

and

Ext!!ext3:	%2∀x y d e.(y≠x ⊃ value(y,assign(x,d,e)) = value(y,e))%1.

.require "memo.pub[let,jmc]" source;
.bb ABSTRACT FORMS


	This note should be read in conjunction with the FOL axioms
in the (nonexistent) file ABSTRA.AX[S76,JMC].  The ideas of abstract forms
are a development from my earlier ideas on %2abstract syntax%1,
%2extensional forms%1 and %2concepts as objects%1.

	An %2abstract form%1 ⊗u contains variables such as ⊗V, ⊗V0, ⊗V1, etc.
and has a value %2value(u,e)%1 in an environment ⊗e.  In some cases,
this value may be the special element ⊗UU, and in this case the value
is regarded as undefined.  The abstractness comes from the fact that
abstract forms will not be defined as strings of symbols, although often
they may be regarded as the equivalence classes determined by some
equivalence relation on strings of symbols.  Even this is not always
possible when, for example, we are dealing with real numbers and take
each number as a ⊗constant (i.e. a particular kind of form), so that
there is a non-denumerable number of forms.  In the cases we have in
mind, classes of abstract forms will be built up inductively from
constants and variables.

	In general the value of an abstract form is another abstract
form, but often its value is a constant.  A constant is an abstract
form ⊗c satisfying

!!a1:	%2∀e.(value(c,e) = c)%1.

.item←0;
Definition #.  An abstract form is called ⊗simple if its value
in an environment ⊗e depends
only on the values of its variables in ⊗e.  Non-simple forms are useful
for merging the idea of an environment or state vector with the idea
of possible world from modal logic.  A concept may have no variables, but
its value may depend on the environment.